A, B:Type, f:(AB), x:A, a:Atom1.
AtomFree(Type;A)  AtomFree(Type;B)  f(x):B>>a  f:AB>>a  x:A>>a 

latex

Definitions	b, x:T>>a, P  Q, x:AB(x), M(a;g;x), x.A(x), f(a), AtomFree(T;x), Atom$n, Type, , s = t, t  T, Unit, left+right, , x:AB(x), x:A. B(x), x:A. B(x), P  Q, {T}
Lemmas	bool wf, assert wf, matters wf, inheres wf, atom-free wf